$\forall$$A$:Type, $x$,$y$:$A$, $P$:($A$$\rightarrow\mathbb{P}$), $i$,$j$:$\mathbb{Z}$.
\\[0ex]($P$(if ($i$ =$_{0}$ $j$) then $x$ else $y$ fi )) $\Rightarrow$ ($P$(if ($i$ =$_{0}$ $j$) then $x$ else $y$ fi ))